00100	AN IDENTITY INVOLVING FUNCTIONS WITH PARAMETERS
00200	
00300	
00400	Consider a domain D and a continuous function F such that
00500	
00600	(1)	F ε Dx(D→D)xD → D.
00700	
00800	The example we have in mind is given by
00900	
01000		F(y,f,x) = if n x then y else a x . f(d x),
01100	
01200	but it is not essential that  F  be this particular function, which
01300	is related to  append by
01400	
01500		append(x,y) = F(y,λx.append(x,y),x).
01600	
01700	We are going to form a function  g  in two ways.  First, we abstract
01800	on  f  and  x  so as to get
01900	
02000		F(y) = λf.λx.F(y,f,x)
02100	
02200	which is in ((D→D)→(D→D)) so that we can apply the  Y  combinator
02300	and form
02400	
02500		g(y) = Y(λf.λx.F(y,f,x)),
02600	
02700	an element of (D→D), and finally
02800	
02900		g = λy.Y(λf.λx.F(y,f,x)),
03000	
03100	an element of (D→(D→D)).
03200	
03300	Another way of getting  g  is to substitute for  f  in (1) a
03400	an expression  f'(y)  where  f'(y) ε (D→D) and hence
03500	f' ε (D→(D→D)), then abstract on f', y and x, getting
03600	
03700		F' = λf'.λy.λx.F(y,f'(y),x)
03800	
03900	where  F' ε ((D→(D→D))→(D→(D→D)), which allows a further abstraction
04000	giving
04100	
04200		g' = Y(F') = Y(λf'.λy.λx.F(y,f'(y),x)),
04300	
04400	with  g' ε (D→(D→D)).
04500	
04600	We assert that  g = g'.  Namely
04700	
04800		g(y,x)	= (λy.Y(λf.λx.F(y,f,x)))(y)(x)
04900	
05000			= Y(λf.λx.F(y,f,x))(x)
05100	
05200			= (λf.λx.F(y,f,x))(Y(λf.λx.F(y,f,x)))(x)
05300	
05400			= F(y,Y(λf.λx.F(y,f,x)),x)
05500	
05600			= F(y,g(y),x),
05700	
05800	whereas
05900	
06000		g'(y,x)	= Y(λf'.λy.λx.F(y,f'(y),x))(y)(x)
06100	
06200			= λf'.λy.λx.F(y,f'(y),x)(Y(λf'.λy.λx.F(y,f'(y),x)))(y)(x)
06300	
06400			= F(y,Y(λf'.λy.λx.F(y,f'(y),x))(y),x)
06500	
06600			= F(y,g'(y),x).
06700	
06800	Thus  g  and  g'  satisfy each others functional equations, and so
06900	by recursion induction and a little hand waving are equal.  Equating
07000	out the right hand sides, we have
07100	
07200		λy.Y(λf.λx.F(y,f,x)) = Y(λf'.λy.λx.F(y,f'(y),x))
07300	
07400	and transforming both sides of the equation, we get
07500	
07600		λy.Y(F(y)) = Y(λf'.λy.F(y)(f'(y))
07700	
07800	and
07900	
08000		B(Y,F) = Y(λf'.λy.S(F,f',y))
08100	
08200			= Y(S(F))
08300	
08400			= B(Y,S)(F),
08500	
08600	and abstracting on  F  which is arbitrary, we get finally
08700	
08800		B(Y) = B(Y,S).
08900	
09000	This identity, which I suppose must be well known is simpler in
09100	its combinatory form than in its λ-calculus form.